module Top(
  input          clock,
  input          reset,
  input          io_in_wr,
  input  [511:0] io_in_wdata,
  input          io_in_rd,
  output [511:0] io_out_rdata,
  output         io_out_empty,
  output         io_out_full,
  input          io_rnd_mark
);
`ifdef RANDOMIZE_MEM_INIT
  reg [511:0] _RAND_0;
`endif // RANDOMIZE_MEM_INIT
`ifdef RANDOMIZE_REG_INIT
  reg [31:0] _RAND_1;
  reg [31:0] _RAND_2;
  reg [511:0] _RAND_3;
  reg [31:0] _RAND_4;
  reg [31:0] _RAND_5;
  reg [31:0] _RAND_6;
`endif // RANDOMIZE_REG_INIT
  wire  resetCounter_clk; // @[Formal.scala 10:36]
  wire  resetCounter_reset; // @[Formal.scala 10:36]
  wire [31:0] resetCounter_timeSinceReset; // @[Formal.scala 10:36]
  wire  resetCounter_notChaos; // @[Formal.scala 10:36]
  reg [511:0] buffer [0:3]; // @[Top.scala 22:19]
  wire  buffer_out_rdata_MPORT_en; // @[Top.scala 22:19]
  wire [1:0] buffer_out_rdata_MPORT_addr; // @[Top.scala 22:19]
  wire [511:0] buffer_out_rdata_MPORT_data; // @[Top.scala 22:19]
  wire [511:0] buffer_MPORT_data; // @[Top.scala 22:19]
  wire [1:0] buffer_MPORT_addr; // @[Top.scala 22:19]
  wire  buffer_MPORT_mask; // @[Top.scala 22:19]
  wire  buffer_MPORT_en; // @[Top.scala 22:19]
  reg [1:0] wrptr; // @[Top.scala 23:22]
  reg [1:0] rdptr; // @[Top.scala 24:22]
  wire [1:0] _pdiff_T_1 = wrptr + 2'h1; // @[Top.scala 25:32]
  wire  pdiff = rdptr == _pdiff_T_1; // @[Top.scala 25:22]
  reg [511:0] out_rdata; // @[Top.scala 27:26]
  reg  out_full; // @[Top.scala 30:25]
  wire  _T_1 = ~io_in_rd; // @[Top.scala 37:29]
  wire  _T_3 = ~io_in_wr; // @[Top.scala 39:15]
  wire  _GEN_0 = ~io_in_wr & io_in_rd ? 1'h0 : out_full; // @[Top.scala 39:37 40:14 42:14]
  wire  _GEN_1 = pdiff & io_in_wr & ~io_in_rd | _GEN_0; // @[Top.scala 37:39 38:14]
  wire [1:0] _rdptr_T_1 = rdptr + 2'h1; // @[Top.scala 59:22]
  wire  _T_9 = ~reset; // @[Top.scala 81:11]
  reg  in_rd_ff1; // @[Top.scala 87:26]
  reg  flag; // @[Top.scala 88:21]
  wire  mark_vld = io_in_wr & io_rnd_mark; // @[Top.scala 95:24]
  wire  check_vld = in_rd_ff1 & out_rdata == 512'h1; // @[Top.scala 96:26]
  wire  _GEN_15 = mark_vld | flag; // @[Top.scala 102:24 103:10 88:21]
  wire  _T_19 = ~mark_vld; // @[Top.scala 109:8]
  wire  _T_20 = ~mark_vld & io_in_wr; // @[Top.scala 109:18]
  ResetCounter resetCounter ( // @[Formal.scala 10:36]
    .clk(resetCounter_clk),
    .reset(resetCounter_reset),
    .timeSinceReset(resetCounter_timeSinceReset),
    .notChaos(resetCounter_notChaos)
  );
  assign buffer_out_rdata_MPORT_en = io_in_rd;
  assign buffer_out_rdata_MPORT_addr = rdptr;
  assign buffer_out_rdata_MPORT_data = buffer[buffer_out_rdata_MPORT_addr]; // @[Top.scala 22:19]
  assign buffer_MPORT_data = io_in_wdata;
  assign buffer_MPORT_addr = wrptr;
  assign buffer_MPORT_mask = 1'h1;
  assign buffer_MPORT_en = io_in_wr;
  assign io_out_rdata = out_rdata; // @[Top.scala 28:16]
  assign io_out_empty = wrptr == rdptr & ~out_full; // @[Top.scala 34:37]
  assign io_out_full = out_full; // @[Top.scala 31:15]
  assign resetCounter_clk = clock; // @[Formal.scala 11:23]
  assign resetCounter_reset = reset; // @[Formal.scala 12:25]
  always @(posedge clock) begin
    if (buffer_MPORT_en & buffer_MPORT_mask) begin
      buffer[buffer_MPORT_addr] <= buffer_MPORT_data; // @[Top.scala 22:19]
    end
    if (reset) begin // @[Top.scala 23:22]
      wrptr <= 2'h0; // @[Top.scala 23:22]
    end else if (io_in_wr) begin // @[Top.scala 46:17]
      if (wrptr < 2'h3) begin // @[Top.scala 47:34]
        wrptr <= _pdiff_T_1; // @[Top.scala 48:13]
      end else begin
        wrptr <= 2'h0; // @[Top.scala 50:13]
      end
    end
    if (reset) begin // @[Top.scala 24:22]
      rdptr <= 2'h0; // @[Top.scala 24:22]
    end else if (io_in_rd) begin // @[Top.scala 57:17]
      if (rdptr < 2'h3) begin // @[Top.scala 58:34]
        rdptr <= _rdptr_T_1; // @[Top.scala 59:13]
      end else begin
        rdptr <= 2'h0; // @[Top.scala 61:13]
      end
    end
    if (reset) begin // @[Top.scala 27:26]
      out_rdata <= 512'h0; // @[Top.scala 27:26]
    end else if (io_in_rd) begin // @[Top.scala 73:17]
      out_rdata <= buffer_out_rdata_MPORT_data; // @[Top.scala 74:15]
    end
    if (reset) begin // @[Top.scala 30:25]
      out_full <= 1'h0; // @[Top.scala 30:25]
    end else begin
      out_full <= _GEN_1;
    end
    if (reset) begin // @[Top.scala 87:26]
      in_rd_ff1 <= 1'h0; // @[Top.scala 87:26]
    end else begin
      in_rd_ff1 <= io_in_rd; // @[Top.scala 98:13]
    end
    if (reset) begin // @[Top.scala 88:21]
      flag <= 1'h0; // @[Top.scala 88:21]
    end else if (check_vld) begin // @[Top.scala 100:18]
      flag <= 1'h0; // @[Top.scala 101:10]
    end else begin
      flag <= _GEN_15;
    end
    `ifndef SYNTHESIS
    `ifdef PRINTF_COND
      if (`PRINTF_COND) begin
    `endif
        if (out_full & ~reset & ~_T_3) begin
          $fwrite(32'h80000002,"Assumption failed\n    at Top.scala:81 assume(!io.in_wr)\n"); // @[Top.scala 81:11]
        end
    `ifdef PRINTF_COND
      end
    `endif
    `endif // SYNTHESIS
    `ifndef SYNTHESIS
    `ifdef PRINTF_COND
      if (`PRINTF_COND) begin
    `endif
        if (io_out_empty & _T_9 & ~_T_1) begin
          $fwrite(32'h80000002,"Assumption failed\n    at Top.scala:84 assume(!io.in_rd)\n"); // @[Top.scala 84:11]
        end
    `ifdef PRINTF_COND
      end
    `endif
    `endif // SYNTHESIS
    `ifndef SYNTHESIS
    `ifdef PRINTF_COND
      if (`PRINTF_COND) begin
    `endif
        if (mark_vld & _T_9 & ~(io_in_wdata == 512'h1)) begin
          $fwrite(32'h80000002,"Assumption failed\n    at Top.scala:107 assume(io.in_wdata === 1.U(WIDTH.W))\n"); // @[Top.scala 107:11]
        end
    `ifdef PRINTF_COND
      end
    `endif
    `endif // SYNTHESIS
    `ifndef SYNTHESIS
    `ifdef PRINTF_COND
      if (`PRINTF_COND) begin
    `endif
        if (_T_20 & _T_9 & ~(io_in_wdata == 512'h0)) begin
          $fwrite(32'h80000002,"Assumption failed\n    at Top.scala:110 assume(io.in_wdata === 0.U(WIDTH.W))\n"); // @[Top.scala 110:11]
        end
    `ifdef PRINTF_COND
      end
    `endif
    `endif // SYNTHESIS
    `ifndef SYNTHESIS
    `ifdef PRINTF_COND
      if (`PRINTF_COND) begin
    `endif
        if (flag & _T_9 & ~_T_19) begin
          $fwrite(32'h80000002,"Assumption failed\n    at Top.scala:113 assume(!mark_vld)\n"); // @[Top.scala 113:11]
        end
    `ifdef PRINTF_COND
      end
    `endif
    `endif // SYNTHESIS
    `ifndef SYNTHESIS
    `ifdef PRINTF_COND
      if (`PRINTF_COND) begin
    `endif
        if (check_vld & resetCounter_notChaos & _T_9 & ~flag) begin
          $fwrite(32'h80000002,"Assertion failed: \n    at Formal.scala:20 cassert(cond, msg)\n"); // @[Top.scala 117:11]
        end
    `ifdef PRINTF_COND
      end
    `endif
    `endif // SYNTHESIS
  end
// Register and memory initialization
`ifdef RANDOMIZE_GARBAGE_ASSIGN
`define RANDOMIZE
`endif
`ifdef RANDOMIZE_INVALID_ASSIGN
`define RANDOMIZE
`endif
`ifdef RANDOMIZE_REG_INIT
`define RANDOMIZE
`endif
`ifdef RANDOMIZE_MEM_INIT
`define RANDOMIZE
`endif
`ifndef RANDOM
`define RANDOM $random
`endif
`ifdef RANDOMIZE_MEM_INIT
  integer initvar;
`endif
`ifndef SYNTHESIS
`ifdef FIRRTL_BEFORE_INITIAL
`FIRRTL_BEFORE_INITIAL
`endif
initial begin
  `ifdef RANDOMIZE
    `ifdef INIT_RANDOM
      `INIT_RANDOM
    `endif
    `ifndef VERILATOR
      `ifdef RANDOMIZE_DELAY
        #`RANDOMIZE_DELAY begin end
      `else
        #0.002 begin end
      `endif
    `endif
`ifdef RANDOMIZE_MEM_INIT
  _RAND_0 = {16{`RANDOM}};
  for (initvar = 0; initvar < 4; initvar = initvar+1)
    buffer[initvar] = _RAND_0[511:0];
`endif // RANDOMIZE_MEM_INIT
`ifdef RANDOMIZE_REG_INIT
  _RAND_1 = {1{`RANDOM}};
  wrptr = _RAND_1[1:0];
  _RAND_2 = {1{`RANDOM}};
  rdptr = _RAND_2[1:0];
  _RAND_3 = {16{`RANDOM}};
  out_rdata = _RAND_3[511:0];
  _RAND_4 = {1{`RANDOM}};
  out_full = _RAND_4[0:0];
  _RAND_5 = {1{`RANDOM}};
  in_rd_ff1 = _RAND_5[0:0];
  _RAND_6 = {1{`RANDOM}};
  flag = _RAND_6[0:0];
`endif // RANDOMIZE_REG_INIT
  `endif // RANDOMIZE
end // initial
`ifdef FIRRTL_AFTER_INITIAL
`FIRRTL_AFTER_INITIAL
`endif
`endif // SYNTHESIS
  always @(posedge clock) begin
    //
    if (out_full & ~reset) begin
      assume(_T_3); // @[Top.scala 81:11]
    end
    //
    if (io_out_empty & _T_9) begin
      assume(_T_1); // @[Top.scala 84:11]
    end
    //
    if (mark_vld & _T_9) begin
      assume(io_in_wdata == 512'h1); // @[Top.scala 107:11]
    end
    //
    if (_T_20 & _T_9) begin
      assume(io_in_wdata == 512'h0); // @[Top.scala 110:11]
    end
    //
    if (flag & _T_9) begin
      assume(_T_19); // @[Top.scala 113:11]
    end
    //
    if (check_vld & resetCounter_notChaos & _T_9) begin
      assert(flag); // @[Top.scala 117:11]
    end
  end
endmodule
